e sends a to i == e':E. loc(e') = i & e' receives a & sender(e') = e 

latex

---

clarification:

es-send-atom-to(es;e;a;i)
== e':es-E(es).
== es-loc(es; e') = i  Id & es-rcv-atom(es;e';a) & es-sender(es; e') = e  es-E(es) 

latex

Definitions	x:A. B(x), P & Q, Id, loc(e), A & B, e receives a, E, sender(e)
FDL editor aliases	es-send-atom-to